The invention relates to systems and methods for verifying the design of digital microcircuits. Such digital microcircuits are now commonplace, and are used in a wide variety of applications, from desktop computers to television controls and common appliances to controllers for machinery, sophisticated weapons systems, and supercomputers. The digital microcircuit design to be tested shall be referred to as the design under test (DUT).
More particularly, the present invention relates to systems and methods applied to a high-level DUT model with the purpose of generating test data that, when applied to a simulation of the DUT, achieves high levels of DUT coverage and therefore has a high likelihood of finding any errors in the DUT.
One known approach has been the use of random input generators to provide input sequences to randomly “drive” the DUT model through the “state space” of possible input and internal register combinations, in the hope of feeding the model a sufficient variety of input combinations to make it possible to identify any errors in the design of DUT. Such methods provide for relatively deep penetration of the space of possible states, but do not provide acceptably broad coverage. This difficulty is aggravated by the observed tendency of even sophisticated random input generators to provide identical or very similar input sequences, or otherwise produce identical or similar DUT register states, on a repeated basis.
Other attempts have involved the use of exhaustive formal search methods. Such methods provide potentially complete coverage of the state space, but for even moderately complex DUTs the state space is so large that time and resource limits preclude the exclusive use of such methods from being effective.
The effect of prior art analysis methods are shown schematically in FIG. 1a. State space 20, which represents in two-dimensional form the space of possible input and register states of the DUT, comprises a plurality of goal states 11 and a start state 10, which typically represents the reset state for the DUT. Trace 15 represents the path through the state space followed by the DUT model in being driven by randomly-generated inputs. Trace 15 wanders relatively deeply through the state space, but without breadth and without apparent direction, and loops back over itself or near to itself at points 23. Trace 15 has intersected two goal states 13 and missed many others. Step traces 31 represent state sequences simulated in the DUT by means of formal methods. Traces 31 have covered a relatively broad but shallow region of the state space, and have located both goal states 13 located within the coverage region.
In speaking of circuit verification by computer simulation, it is useful to define several terms. A goal or coverage state is any state which is desired to be reached under test conditions to provide adequate coverage of the DUT. Typically there exist a number of tasks a circuit is designed to do, and a number of things that are recognized as undesirable for the circuit to do—that is, there exist a number of circuit states which it is desirable or undesirable for the circuit to assume. Usually a set or record of such desirable and undesirable states is maintained and used as a basis for coverage measurement and for analysis of the quality of testing. While most generally a goal state completely defines the complete register contents of the DUT, a goal state definition may specify only a subset of the register bits, and therefore specifies a boolean hyper-cube of specific states.
A formal simulation method is any method used to systematically—as opposed to randomly—simulate different states of a DUT. In particular, formal simulation methods include formal reachability methods. Formal reachability methods, in the context of this application, include any exhaustive or other mathematical techniques for finding input assignments for causing a state machine, or a state machine model, to transition from a starting state to some other state. Examples of formal simulation methods include symbolic simulation and SAT bounded model checking techniques, as disclosed herein.